R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
21(c(1(x1))) → R1(1(x1))
21(L(x1)) → 21(x1)
21(c(0(x1))) → 01(0(x1))
21(c(1(x1))) → 01(R(1(x1)))
01(L(x1)) → 21(R(x1))
R1(1(x1)) → 31(x1)
R1(3(x1)) → 31(R(x1))
31(L(x1)) → 31(x1)
R1(3(x1)) → R1(x1)
R1(2(x1)) → 21(R(x1))
R1(2(x1)) → R1(x1)
01(L(x1)) → R1(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
21(c(1(x1))) → R1(1(x1))
21(L(x1)) → 21(x1)
21(c(0(x1))) → 01(0(x1))
21(c(1(x1))) → 01(R(1(x1)))
01(L(x1)) → 21(R(x1))
R1(1(x1)) → 31(x1)
R1(3(x1)) → 31(R(x1))
31(L(x1)) → 31(x1)
R1(3(x1)) → R1(x1)
R1(2(x1)) → 21(R(x1))
R1(2(x1)) → R1(x1)
01(L(x1)) → R1(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
31(L(x1)) → 31(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
31(L(x1)) → 31(x1)
The value of delta used in the strict ordering is 4.
POL(31(x1)) = (4)x_1
POL(L(x1)) = 1 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
21(L(x1)) → 21(x1)
21(c(0(x1))) → 01(0(x1))
01(L(x1)) → 21(R(x1))
21(c(1(x1))) → 01(R(1(x1)))
R1(3(x1)) → R1(x1)
R1(2(x1)) → 21(R(x1))
R1(2(x1)) → R1(x1)
01(L(x1)) → R1(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R1(2(x1)) → 21(R(x1))
R1(2(x1)) → R1(x1)
Used ordering: Polynomial interpretation [25,35]:
21(L(x1)) → 21(x1)
21(c(0(x1))) → 01(0(x1))
01(L(x1)) → 21(R(x1))
21(c(1(x1))) → 01(R(1(x1)))
R1(3(x1)) → R1(x1)
01(L(x1)) → R1(x1)
The value of delta used in the strict ordering is 8.
POL(21(x1)) = (2)x_1
POL(1(x1)) = x_1
POL(c(x1)) = x_1
POL(01(x1)) = (2)x_1
POL(3(x1)) = x_1
POL(2(x1)) = 4 + x_1
POL(L(x1)) = x_1
POL(b(x1)) = 0
POL(0(x1)) = 4 + x_1
POL(R1(x1)) = (2)x_1
POL(R(x1)) = x_1
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
3(L(x1)) → L(3(x1))
R(b(x1)) → c(1(b(x1)))
0(L(x1)) → 2(R(x1))
2(c(1(x1))) → c(0(R(1(x1))))
3(c(x1)) → c(1(x1))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
21(L(x1)) → 21(x1)
21(c(1(x1))) → 01(R(1(x1)))
01(L(x1)) → 21(R(x1))
21(c(0(x1))) → 01(0(x1))
R1(3(x1)) → R1(x1)
01(L(x1)) → R1(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
R1(3(x1)) → R1(x1)
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R1(3(x1)) → R1(x1)
The value of delta used in the strict ordering is 4.
POL(3(x1)) = 1 + (4)x_1
POL(R1(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
21(L(x1)) → 21(x1)
21(c(0(x1))) → 01(0(x1))
01(L(x1)) → 21(R(x1))
21(c(1(x1))) → 01(R(1(x1)))
R(2(x1)) → 2(R(x1))
R(3(x1)) → 3(R(x1))
R(1(x1)) → L(3(x1))
3(L(x1)) → L(3(x1))
2(L(x1)) → L(2(x1))
0(L(x1)) → 2(R(x1))
R(b(x1)) → c(1(b(x1)))
3(c(x1)) → c(1(x1))
2(c(1(x1))) → c(0(R(1(x1))))
2(c(0(x1))) → c(0(0(x1)))